box!(${\it Run}$;$P$)(${\it sys}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\exists$${\it run}$:${\it Run}$. (${\it sys}$(${\it run}$))) \& ($\forall$${\it run}$:${\it Run}$. (${\it sys}$(${\it run}$)) $\Rightarrow$ ($P$(${\it run}$)))